T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} .
(x changed before e)  e'<e.(es-after(es; x; e') = es-when(es; x; e')  T) 

latex

Definitions

x:A. B(x), x changed before e, change-to(x;e), t  T, P  Q, P  Q, prop{i:l}, P  Q, EqDecider(T), es-dtype(es; i; x; T), P  Q, P  Q, x. t(x), A c B, b, isl(x), tt, ff, if b then t else f fi , True, e<e'.P(e), x:A. B(x), A, T, x(s), False, es-locl(es; e; e'), @e(xv), ee'.P(e), SqStable(P), sq_type(T), guard(T)

Lemmas

es-E wf, es-dtype wf, es-loc wf, Id wf, event system wf, deq wf, bool wf, iff wf, assert wf, es-isconst wf, es-vartype wf, existse-before wf, es-change-to wf, es-when wf, subtype rel self, alle-between3 wf, not wf, es-first wf, alle-le wf, true wf, es-after wf, false wf, es-locl wf, es-next, es-le weakening, es-after-pred2, sq stable from decidable, decidable assert, es-le-loc, es-loc-pred, es-locl-iff, Id sq, sq stable subtype rel